\documentclass[11pt,a4paper]{article}

\usepackage{url,,}
\usepackage[pdftex]{graphicx}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsmath}

\usepackage{hyperref}	% this package is used to create hyperlinks to sections, which are reflected in the table of contents
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{multirow}
\usepackage{listings}
\usepackage{fullpage}
\usepackage{fancyhdr,a4wide}
\usepackage{makeidx}
\usepackage{placeins}

\lstset{ %
% language=VHDL,                % choose the language of the code
basicstyle=\footnotesize,       % the size of the fonts that are used for the code
showstringspaces=false,         % underline spaces within strings
%numbers=left,                   % where to put the line-numbers
%numberstyle=\footnotesize,      % the size of the fonts that are used for the line-numbers
%stepnumber=1,                   % the step between two line-numbers. If it's 1 each line will be numbered
%numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
showspaces=false,               % show spaces within strings adding particular underscores
showtabs=false,                 % show tabs within strings adding particular underscores
escapeinside={\%*}{*)}          % if you want to add a comment within your code
}

\begin{document}	

\begin{titlepage}

\thispagestyle{fancy}
\lhead{}
\chead{
\large{\textit{
Informatics and Mathematical Modelling\\
Technical University of Denmark}}}
\rhead{}
\rule{0pt}{50pt}
\vspace{3cm}

\begin{center}

 	\Huge{\textbf{02241 : Robust Programming in .NET}}\\
 	\vspace{1.5cm}
 	\huge{Modelling and Simulation of Railway Systems\\ for DSB}\\
 	\vspace{0.5cm}
 	\LARGE{An Analysis and Design Report}\\
 	\vspace{0.5cm}
\end{center}

\vspace{4cm}

\begin{flushright}
	\LARGE{Markku Eerola (s053739)}\\
	\vspace{0.3cm}
	\LARGE{Rajesh Bachani (s061332)}\\
	\vspace{0.3cm}
	\LARGE{Jakob Hommelhoff Jensen (s071312)}\\

\end{flushright}
\vfill
\rule{0pt}{0pt}
\cfoot{\today}
\end{titlepage}


%-----------------------------------------------------------
\newpage 
\tableofcontents

\newpage 
\section{Introduction}

Danish State Railway, DSB, is the largest Danish train operating company. Due to constant problems with the train networks under the DSB, the company is planning to design its networks in a fresh way. The company wishes to be provided with a modelling system, which would help visualize the entire network under the company's horizon. In addition, the company wishes to be provided with a simulation system, which would be able to check and detect problems, with trains specified to be running on particular routes. Thirdly, the company would also want an extended system, which would help in determining train timings, and inform possible collisions of trains on same tracks, according to the specified train timings. Overall, the purpose of the system is to help DSB build a robust and systematic network, which hopefully should be free of any kind of problems, and make the design of the entire network and trains running on them, easy.

In the first section, we explain the problem in much detail, and give an analysis of the requirements specifications. The second section contains the design of the system, which should support these requirements. In the third section, we give a brief overview of how far we are in the development of the system. This section is completely aimed for the course 02241, while the first two sections are more as a feedback and update to DSB.

\section{Requirements Analysis}

This section contains the analysis of the system that DSB wishes to be provided with. The section is further structured into three sections. The first section contains the description and analysis of how the railway network would be modelled in the system. The second section consists of the specifications for the train routes. The third section touches upon the extensions which are possible in the system, which would help DSB fix timings for trains and ensure that there would be no collisions. We propose some ideas to DSB for their approval, here in the third section.

\subsection{Modelling the tracks}
The engineers at DSB have decided that the new system of railways would have three kinds of tracks. These three tracks are supposed to be the building blocks for the entire network. These tracks are,
\begin{itemize}
\item \textit{Straight Track} This track connects two stations. A straight track between stations A and B indicates a direct connection between these stations.
\item \textit{Switch Track} This track forms a switch between three stations. Any train running on this track from one end would have the possibility of switching path to one of the two stations on the other end. It is assumed that the `node' in the center of the switch track is not a station. 
\item \textit{End Track} An end track is simply a track which starts from one station and ends without connecting to any other station. The end track would always connect a station to an end point, which is not a station.
\end{itemize}

% Following is an illustration of these three kinds of tracks.

% Insert an image of these tracks

Having said this, we need to specify a way by which DSB could model its network of stations and the kinds of tracks connecting them. This is done using a simple grammar, which is mentioned in the problem description document \cite{1}. Assuming the identifier is a unique way to identify a station, the basic keywords in the grammar are,
\begin{itemize}
\item \verb,STAT, followed by the name of the station and an identifier, indicates a station.
\item \verb,CONN, followed by two identifiers, indicates a connection between the identifiers. A connection directly refers to a straight track (if both the identifiers are stations, and none is a `node').
\item \verb,END, followed by an identifier of a station, indicates that one connection to the identifier ends. An end keyword directly refers to an end track.
\end{itemize}
\noindent As we can see, the straight and end tracks can be directly constructed using the keywords \verb,STAT, and \verb,CONN,. A switch track cannot be directly constructed using one keyword, but is constructed using more than one of these keywords. A simple example for switch tracks is shown here,
\begin{verbatim}
STAT Hellerup h
STAT Lyngby l
STAT Klampenborg k
CONN h b
CONN b l
CONN b k
\end{verbatim}

Here, we have three stations specified by the \verb'STAT' statements. The \verb,CONN, statements use the stations, and also introduce an identifier `b' which is not a station. It can be clearly seen that the specification above represents a switch track, where `b' is the `node' which connects the three stations.\\
\noindent To brief it up, there are only three kinds of tracks that are used to define the entire track network. These tracks are specified using the grammar in \cite{1}. 

\subsection{Defining train routes}

Once the track network is defined, routes taken by various trains are mapped on to it. These are done using the keyword \verb,ROUTE,, and all the permissible routes are supplied in the specification file. The grammar for the train routes specification is also provided in \cite{1}.

A simple example of a route specification would be,
\begin{verbatim}
ROUTE h b STOP l STOP
\end{verbatim}
This means that there is a train which goes from `h' to `b' and stops. Then is continues from `b' to `l' and stops again. Such routes would be considered valid only if there are stations or nodes with the identifiers given in the route. The system would check the validity of the routes in the specification, and notify the user, which is DSB engineers in our case, that the specification is faulty at the specified place. 
Some specifications included in \cite{1} are,
\begin{itemize}
\item Trains can change directions only when they are stopped. In the simple case, this means that if a train wants to go back on some portion of the path it already travelled, it would be indicated by a \verb,STOP, in the route specification of that train. 
\item Switch tracks have some sense of direction in the branches.
\end{itemize}


\subsection{Extension: Simulation of trains}
Once the specification of the train routes is done, we can simulate the trains on the tracks, by specifying exact timings. For all the routes of trains, the engineers could specify exact time of the train arriving at that point, and then departing from that point. This could be represented by the following example,
\begin{verbatim}
ROUTE 0 h 34 b STOP 55 71 l STOP
\end{verbatim}
The above example could be read as: Train starts at `h' at time 0, reaches `b' at time 34 and stops there. Then it continues starting at time 55 and stops at `l' at time 71.

Once such a specification is provided for all the routes, the system would be able to check if there are any collisions occuring between any two tracks. If a collision is detected, the system would recommend changing the timings of the routes in consideration.

\section{Design}
The system design would be object-oriented, since this would ease visualizing the system. There would be entities for the various kinds of tracks, which include straight, switch and end tracks. Instances of these entities based on the specification of the network, would serve as the basis for all the functionalies provided by the system, and also including the extensions for the system. This is because, the entire network would be represented by just a collection of instances of these entities.

The system would be supplied with atleast the following two files, to start with. 
\begin{itemize}
\item \textit{tracks.txt} which would contain the network specification
\item \textit{routes.txt} which would contain the train routes specification
\end{itemize}

In addition, we could have more input files required based on the extensions. As an example, a \textit{times.txt} file would be used, which would hold the enhanced route specification containing the time schedules of trains.

\noindent Based on these files, the first job that the system would do is understand the tracks specification from the \textit{tracks.txt} file. We have tried to modularize the job as much as we can, such that there is a required and ensured property, by default, which can be directly mapped to SPEC\# implementation. The following tasks are to be done here in this job,
\begin{itemize}
\item Read the file containing the specification
\item Verify the specification for syntactic correctness
\item Verify the specification for semantic correctness
\item If the specification is correct, generate the corresponding tracks
\end{itemize}

We have ensured some of the constraints on the system using SPEC\#. As we get more into the implementation, we hope that more situations would be clear where SPEC\# could prove to be very helpful in easing the design of the system. 
\begin{itemize}
\item Checked exceptions are used to indicate admissible errors in some functions. As an example, if the input file does not exist, the input handler could throw a checked exception. This is fairly simple in Spec\#.
\item The input handler would read the track specification just for syntactic correctness, and it could return null data structures in case the input file contains nothing. An identifier would indicate if the tracks are read or not read. The next step, which is verifying tracks semantically, would then require in the contract that the identifier shows that tracks are read.
\item We could ensure that a straight track or switch track instance is not created with two of the stations being the same. This case should not be valid, and it can be checked as a required contract for calling the constructors of these entities.
\item Again, using the required contract, we could make sure that the verification of the track specification semantically is not done on null data structures, if the input file does not contain anything.
\item We intend to keep an identifier which would be set to true if the semantic verification is successful. The value of this identifier is a required contract for the system to geenrate the track instances. This is again implemented using SPEC\#.
\end{itemize}\\

\newline
The second job that the system would do is to read the \textit{routes.txt} file, containing specification for the train routes. The system has to read every route, and then verify if it could be mapped to a path in the tracks network. 
For every jump that the train route specifies, the tracks network is checked if there exists such a connection. If there is a connection, either in straight, switch or end track, which allows such a jump, it is fine. Otherwise, the jump is considered invalid, leading to the entire route being considered invalid.

\section{Preview on Implementation}

So far, we have implemented the part of the system which reads the track specification, verifies it syntactically and semantically, and generates the track instances, if the verification is successful. The checks which are mentioned in the design section are implemented. Though, still there need some more checks to be implemented.

In order to organize our code, we have created a SVN repository on Google Code to serve as source control \cite{svn}.
\newpage
\nocite{barnett-spec}
\nocite{leino-exception}
\bibliographystyle{plain}
\bibliography{DesignandAnalysisReport}

\end{document}